Nuprl Lemma : kind_wf
0,22
postcript
pdf
E
:Type,
info
:(
E
(Id
Id+(IdLnk
E
)
Id)),
e
:
E
. kind(
e
)
Knd
latex
Definitions
kind(
e
)
,
locl(
a
)
,
rcv(
l
,
tg
)
,
1of(
t
)
,
2of(
t
)
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
Id
,
IdLnk
,
t
T
Lemmas
IdLnk
wf
,
Id
wf
,
pi2
wf
,
pi1
wf
,
rcv
wf
,
locl
wf
origin
E:Type, info:(E
(Id
Id+(IdLnkE)Id)), e:E. kind(e) 
Knd E:Type, info:(E(IdId+(IdLnkE)Id)), e:E. kind(e) Knd 
x. t(x)x:A. B(x) T